#!/bin/sh

./rundir smtlib-parser "" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution

./rundir interpolation "" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -constructProofs=always -generateTriggers=none

./rundir werePrincess ""

./rundir allSettings "1" -logo +assert -timeout=30000 -clausifier=none -posUnitResolution -constructProofs=never -generateTriggers=none
./rundir allSettings "2" -logo +assert -timeout=30000 -clausifier=simple -posUnitResolution -constructProofs=never -generateTriggers=none
./rundir allSettings "3" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -constructProofs=never -generateTriggers=none
./rundir allSettings "4" -logo +assert -timeout=30000 -clausifier=simple +posUnitResolution -constructProofs=never -generateTriggers=none
./rundir allSettings "5" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -constructProofs=never -generateTriggers=total
./rundir allSettings "6" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -constructProofs=never -generateTriggers=all

./rundir onlyUnitResolution "" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -generateTriggers=none
./rundir onlyUnitResolution "" -logo +assert -timeout=30000 -clausifier=simple +posUnitResolution -generateTriggers=none
./rundir onlyUnitResolution "" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -generateTriggers=all
./rundir onlyUnitResolution "" -logo +assert -timeout=30000 -clausifier=simple +posUnitResolution -generateTriggers=all

./rundir onlyClausification "" -logo +assert -timeout=30000 -clausifier=simple +posUnitResolution -generateTriggers=none

./rundir mostGeneralConstraint "" -logo +assert -timeout=30000 +posUnitResolution +mostGeneralConstraint -generateTriggers=none

./rundir special "" -logo +assert -generateTriggers=none

./rundir lira "" -logo +assert -timeout=120000 -assert -clausifier=none -posUnitResolution -simplifyConstraints=lemmas -generateTriggers=none

./rundir unprovable "1" -logo +assert -timeout=30000 -clausifier=none -posUnitResolution -generateTriggers=none
./rundir unprovable "2" -logo +assert -timeout=30000 -clausifier=simple -posUnitResolution -generateTriggers=none
./rundir unprovable "3" -logo +assert -timeout=30000 -clausifier=none +posUnitResolution -generateTriggers=none
./rundir unprovable "4" -logo +assert -timeout=30000 -clausifier=simple +posUnitResolution -generateTriggers=none

